Nuprl Lemma : comb_for_cons_wf_listp
4,23
postcript
pdf
(
A
,
l
,
x
,
z
.
x
.
l
)
A
:Type
(
A
List)
A
True
A
List
latex
Definitions
True
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
cons
wf
listp
,
squash
wf
,
true
wf
origin
A,l,x,z. x.l) 
A:Type
(A List)A
TrueA List
A,l,x,z. x.l) A:Type(A List)ATrueA List T
x:A. B(x)T